es:ES, l1, l2:IdLnk, tg1, tg2:Id.
es-responsive(es;l1;tg1;l2;tg2)
 (f:({e:E| kind(e) = rcv(l1,tg1)  Knd }{e:E| kind(e) = rcv(l2,tg2)  Knd }).
 (Bij({e:E| kind(e) = rcv(l1,tg1)  Knd }; {e:E| kind(e) = rcv(l2,tg2)  Knd }; f)) 

latex

Definitions	e=rcv(l,tg). P(e), e=rcv(l,tg). P(e), P & Q, es-responsive(es;l1;tg1;l2;tg2), ES, t  T, IdLnk, Id, x:A. B(x), E, Knd, Bij(A; B; f), x:A. B(x), P  Q, sender(e), rcv(l,tg), kind(e), (e <loc e'), e  e' , , 1of(t), A & B, Prop, {T}, b, Unit, x. t(x), P  Q, if b t else f fi, Surj(A; B; f), Inj(A; B; f), P  Q, False, A, isrcv(e), True, T, SqStable(P), Dec(P), P  Q, Trans x,y:T. E(x;y)
Lemmas	es-locl-trans, decidable equal Kind, es-le-not-locl, sq stable from decidable, decidable assert, assert wf, es-isrcv wf, es-le-loc, es-loc-pred, es-loc-rcv, es-axioms, biject wf, pi1 wf, it wf, es-le wf, es-locl wf, es-sender wf, es-kind-rcv, es-E wf, Knd wf, es-kind wf, rcv wf, es-responsive wf, Id wf, IdLnk wf, event system wf